$\forall$$A$, $B$:Realizer.
\\[0ex]($\neg$($\uparrow$Rplus?($A$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$Rplus?($B$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$Rnone?($A$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$Rnone?($B$)))
\\[0ex]$\Rightarrow$ (R{-}base{-}domain($A$) = R{-}base{-}domain($B$) $\in$ ($n$:$\mathbb{Z}$ $\times$ base{-}domain{-}type($n$)))
\\[0ex]$\Rightarrow$ (R{-}loc($A$) = R{-}loc($B$) $\in$ Id)
\\[0ex]$\Rightarrow$ ($\exists$$x$:MaName. (($x$ $\in$ R{-}names($A$)) \& ($x$ $\in$ R{-}names($B$))))